w\_locl($w$;$x$;$y$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$x$ $\lambda$$x$,$y$. $\neg$first($y$) \& $x$ $=$ pred($y$)\^{}+ $y$